@david-christiansen I think the tutorial chapter is now sort of a mixture between a simple API reference listing and a top-down, tutorial-style blog post. It is not unlike the grind chapter or the Natural numbers section, I think. I suppose I could just add another section "API reference" for listing more of the API that is not yet covered by the tutorial?

@sgraf812 I made a number of updates, and it's ready for you to check them. Thanks for your patience here!

Thanks, David! I gave it a full read and made some mostly minor edits. One edit wasn't minor; I un-TODO'd the mvcgen invariants? paragraph because it is fully supported since 4.24. In the HTML view, the suggestion it reports was hidden under the tooltip for the proof state, so I decided it's simpler to use #guard_msgs (info). Wouldn't mind if you double-checked that for a better solution.

Otherwise LGTM :) Thank you for contributing the nice technical introduction sections!

When I read this kind of document I attempt to have a mental model of a member of the target audience, and then be on the lookout for background they won't have.

I think it's ready to go now. Thanks again for your patience!

Preview for this PR is ready! 🎉 (also as a proofreading version). built with commit b6b2313.